loc:Id, ds:x:Id fp Type, knd:Knd, T:Type, x:Id, f:(State(ds)TDeclaredType(ds;x)).
@loc effect knd(v:T)  x := f State(ds) v   Realizer 

latex

Definitions	Knd, t  T, type List, Id, x:AB(x), IdLnk, left+right, Type, Prop, x:AB(x), x:A. B(x), State(ds), x. t(x), a:A fp B(a), DeclaredType(ds;x), Unit, rec(x.A(x)), <a,b>, inl(x), inr(x), @loc effect knd(v:T)  x := f State(ds) v , Realizer
Lemmas	unit wf, decl-type wf, fpf wf, decl-state wf, IdLnk wf, Id wf, Knd wf